Nuprl Lemma : cmseq_wf
11,40
postcript
pdf
from
,
to
:Id,
num
:
. cmseq(
from
;
to
;
num
)
chain_master()
latex
Definitions
cmseq(
from
;
to
;
num
)
,
chain_master()
,
t
T
,
x
:
A
.
B
(
x
)
Lemmas
Id
wf
,
nat
wf
origin
from, to:Id, num:
. cmseq(from;to;num) 
chain_master() from, to:Id, num:. cmseq(from;to;num) chain_master() Tx:A. B(x)